Deadlock-freeness (with probability)

Given P() as a process, the following assertion asks if P() is deadlock-free or not(P() is deadlock-free with max/min/both probability).

#assert P() deadlockfree (with pmin/ pmax/ prob);

Reachability (with probability)

Given P() as a process, the following assertion asks if P() can reach a state at which some given condition is satisfied(P() can reach a state with max/min/both probability).

#assert P() reaches cond (with pmin/ pmax/ prob);

Linear Temporal Logic (LTL) (with probability)

In PAT, we support the full set of LTL syntax. Given a process P(), the following assertion asks whether P() satisfies the LTL formula(P() can satisfy an LTL formula with max/min/both probability).

#assert P() |= F (with pmin/ pmax/ prob);

where F is an LTL formula.

Refinement Checking (with probability)

PAT now also supports refinement checking in PRTS. User could define a non-probabilistic property using CSP# as a specificaiton. Then PAT could tell users if the system behaves under the constraint of the specification(the system behaves under the constraint of the specification with max/min/both probability).

          #assert Implementation() refines Spec() (with prob/ pmin/ pmax);

where Spec() is the user-defined specification.

Timed Refinement Checking

Similiarly to RTS module, PRTS also supports timed refinement checking. This property allows user to define the specification which has real-time features and check if the implementation could work under the constraint of timed specification:

#assert Implementation() refines<T> TimedSpec() ;

where TimedSpec() is the user-defined timed specification.

Timed Refinement Checking with probability(In Progress)

We are working to specify some unique properties in PRTS which could not be handled by other modules. Timed probabilistic refinement checking allows users to check the max/min/both probability with which implementation could work under the constraint of timed specification.

          #assert Implementation() refines<T> TimedSpec() with prob/ pmin/ pmax;

where Spec() is the user-defined specification.

These properties a just a part of that PRTS could support; and we are exploring more systems to find more and more suitable properties that could be verified in PRTS module.